The present invention relates generally to the field of hardware and software function verification, and more particularly to determining concrete counterexamples of liveness properties.
Regarding the verification of system hardware and software components, two types of properties are prevalent. One property is referred to as a safety property, and the other is referred to as a liveness property. A safety property asserts that during operation of the hardware or software component, something bad should never happen. In LTL (Linear Time Temporal Logic) safety properties are often expressed in the form: G (!P), which may be expressed as, (globally), “it is always the case that P never happens”, for some combinational or bounded temporal condition P. This is illustrated by considering an equivalence checking problem in which an optimized design is checked against a reference model. The outputs of both the optimized and reference instances should always be equal, therefore P would express the bitwise inequality of these two designs, and it would be expected that the inequality would never happen G (!P).
A liveness property asserts that “something good eventually must happen”. In LTL, such properties can be expressed in form: GF (P), which may be expressed as, “it is always the case that sometime in the future, P occurs”. To illustrate this, in case of an arbiter verification, every request should eventually be acknowledged, for example, granting the request. Liveness verification often involves fairness constraints, which confirm the validity of a failure by enforcing certain conditions to hold. For example, a system with various priorities associated with requests may need to enforce that higher-priority requests eventually allow the system to grant lower-priority requests, without which liveness checking of lower-priority requests would fail. The eventual granting of lower-priority requests of the example is a fairness condition enforced in a liveness property verification. Safety properties typically contain a finite length counterexample illustrating a failure condition. Whereas for liveness properties, counterexamples are typically infinite in length. Liveness verification is very crucial for systems such as arbiters, which typically restrict access to shared resources in the microprocessors.